Assertion languages, which are widely used in the electronic chip design industry in designing circuits, allow circuit designers to describe acts of a circuit and embed information into their designs to facilitate verification using computer models. Assertions are built up using Boolean expressions, or conditions, which are evaluated at certain times during the execution of the design. For example, the assertion “always C”, where C is a condition, says that C must be true in each clock cycle. More complex, multi-cycle behavior can be expressed with sequences, which consist of a list of conditions that may or must be true in successive cycles, such as c1, c2, c3, . . . , cn, where c1 through cn are conditions that may or must be true in cycles 1 through n.
A procedure, called formal analysis, is used by the circuit design industry in verifying assertions based on a set of constraints or verification requirements. Assertions that are being verified need to satisfy the constraints. A formal analysis tool tries to disprove assertions by analyzing the circuit design and the constraints. If the formal analysis tool cannot disprove an assertion by finding a failure under the constraints, then the tool reports a passing result, which means that no failures were found in this design using the constraint set.
The selection and use of constraints in formal analysis directly affect the scope of design verifications. In certain extreme cases, logically flawed constraints or overly strict constraints allow only a small portion, or even nothing, in a circuit design to be explored. This type of constraints or verification requirements is “over-constrained,” which is usually caused by errors in the constraints specification. Over-constrained verification requirements lead to unexpected results. The formal analysis tool cannot satisfy conflicting constraints. Tools can report assertion failures only if those failures satisfy the constraints. In the absence of failures, tools report a passing result.
For instance, the following PSL (Property Specification Language) constraints illustrate an example of over-constrained verification requirements:
Constraint A (signal a should always be high (1/true) for all times):                assume_always_a: assume always (a)        
Constraint B: (Assume that signal a should never be high for all times):                assume_never_a: assume never (a)The first constraint states that “a” should always be high, and the second constraint says “a” should never be high. If both constraints are used in a formal analysis where signal “a” is referenced in the fan-in cone of an assertion, an over-constrained situation occurs. It is not possible to satisfy both constraints at the same time, as they basically express the exact opposite behavior. In this case, the over-constrained situation is a result of conflicting statements related to a common signal a, and does not include any logic of the design.        
In the following example, two PSL constraints and a Verilog assignment to a wire b, shows another type of over-constrained situation:
b takes the inverted value of a. In other words b is not a.                assign b=! a;        
Assume that signal a should always be high (1/true) for all times.                assume_always_a: assume always (a);        
Assume that signal b should always be high (1/true) for all times.                assume_never_a: assume always (b);In this case, the conflict is caused by a combination of the constraints and the logic of the design (assignment to b).        
For illustration purpose, the above examples use very simple scenarios to explain the mechanism of over-constrained situations. In real world, however, circuit designs involve many complex constraints and driving logic. Detection of and debugging over-constrained situations become a very hard task.
Therefore, there is a need for an effective and automatic approach for detecting and debugging over-constrained situations. It is still desired to obtain more useful information related to the occurrence of over-constrained events, to assist debugging.